(set-logic QF_UF)
(set-info :source |
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
 for more information. 

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-fun f1 (U U) U)
(declare-fun p2 (U U U) Bool)
(declare-fun c3 () U)
(declare-fun c4 () U)
(declare-fun c5 () U)
(declare-fun c_0 () U)
(declare-fun c_1 () U)
(declare-fun c_2 () U)
(declare-fun c_3 () U)
(declare-fun c_4 () U)
(assert (let ((?v_275 (f1 c_0 c_0))) (let ((?v_300 (not (= c_0 ?v_275))) (?v_280 (f1 c_1 c_0)) (?v_285 (f1 c_2 c_0)) (?v_290 (f1 c_3 c_0)) (?v_295 (f1 c_4 c_0)) (?v_276 (f1 c_0 c_1)) (?v_281 (f1 c_1 c_1))) (let ((?v_301 (not (= c_1 ?v_281))) (?v_286 (f1 c_2 c_1)) (?v_291 (f1 c_3 c_1)) (?v_296 (f1 c_4 c_1)) (?v_277 (f1 c_0 c_2)) (?v_282 (f1 c_1 c_2)) (?v_287 (f1 c_2 c_2))) (let ((?v_302 (not (= c_2 ?v_287))) (?v_292 (f1 c_3 c_2)) (?v_297 (f1 c_4 c_2)) (?v_278 (f1 c_0 c_3)) (?v_283 (f1 c_1 c_3)) (?v_288 (f1 c_2 c_3)) (?v_293 (f1 c_3 c_3))) (let ((?v_303 (not (= c_3 ?v_293))) (?v_298 (f1 c_4 c_3)) (?v_279 (f1 c_0 c_4)) (?v_284 (f1 c_1 c_4)) (?v_289 (f1 c_2 c_4)) (?v_294 (f1 c_3 c_4)) (?v_299 (f1 c_4 c_4))) (let ((?v_304 (not (= c_4 ?v_299))) (?v_0 (p2 c_0 c_0 c_0)) (?v_1 (= c_0 c_0))) (let ((?v_2 (not ?v_0)) (?v_16 (= c_1 c_0)) (?v_15 (p2 c_0 c_1 c_0))) (let ((?v_17 (not ?v_15)) (?v_3 (= c_0 c_1)) (?v_7 (p2 c_0 c_0 c_1))) (let ((?v_8 (not ?v_7)) (?v_20 (= c_2 c_0)) (?v_45 (p2 c_0 c_2 c_0))) (let ((?v_46 (not ?v_45)) (?v_4 (= c_0 c_2)) (?v_12 (p2 c_0 c_0 c_2))) (let ((?v_9 (not ?v_12)) (?v_23 (= c_3 c_0)) (?v_55 (p2 c_0 c_3 c_0))) (let ((?v_56 (not ?v_55)) (?v_5 (= c_0 c_3)) (?v_13 (p2 c_0 c_0 c_3))) (let ((?v_10 (not ?v_13)) (?v_26 (= c_4 c_0)) (?v_65 (p2 c_0 c_4 c_0))) (let ((?v_66 (not ?v_65)) (?v_6 (= c_0 c_4)) (?v_14 (p2 c_0 c_0 c_4))) (let ((?v_11 (not ?v_14)) (?v_18 (= c_1 c_1)) (?v_29 (p2 c_0 c_1 c_1))) (let ((?v_19 (not ?v_29)) (?v_30 (= c_2 c_1)) (?v_51 (p2 c_0 c_2 c_1))) (let ((?v_47 (not ?v_51)) (?v_31 (= c_3 c_1)) (?v_61 (p2 c_0 c_3 c_1))) (let ((?v_57 (not ?v_61)) (?v_32 (= c_4 c_1)) (?v_71 (p2 c_0 c_4 c_1))) (let ((?v_67 (not ?v_71)) (?v_21 (= c_1 c_2)) (?v_33 (p2 c_0 c_1 c_2))) (let ((?v_22 (not ?v_33)) (?v_34 (= c_2 c_2)) (?v_52 (p2 c_0 c_2 c_2))) (let ((?v_48 (not ?v_52)) (?v_35 (= c_3 c_2)) (?v_62 (p2 c_0 c_3 c_2))) (let ((?v_58 (not ?v_62)) (?v_36 (= c_4 c_2)) (?v_72 (p2 c_0 c_4 c_2))) (let ((?v_68 (not ?v_72)) (?v_24 (= c_1 c_3)) (?v_37 (p2 c_0 c_1 c_3))) (let ((?v_25 (not ?v_37)) (?v_38 (= c_2 c_3)) (?v_53 (p2 c_0 c_2 c_3))) (let ((?v_49 (not ?v_53)) (?v_39 (= c_3 c_3)) (?v_63 (p2 c_0 c_3 c_3))) (let ((?v_59 (not ?v_63)) (?v_40 (= c_4 c_3)) (?v_73 (p2 c_0 c_4 c_3))) (let ((?v_69 (not ?v_73)) (?v_27 (= c_1 c_4)) (?v_41 (p2 c_0 c_1 c_4))) (let ((?v_28 (not ?v_41)) (?v_42 (= c_2 c_4)) (?v_54 (p2 c_0 c_2 c_4))) (let ((?v_50 (not ?v_54)) (?v_43 (= c_3 c_4)) (?v_64 (p2 c_0 c_3 c_4))) (let ((?v_60 (not ?v_64)) (?v_44 (= c_4 c_4)) (?v_74 (p2 c_0 c_4 c_4))) (let ((?v_70 (not ?v_74)) (?v_75 (p2 c_1 c_0 c_0))) (let ((?v_76 (not ?v_75)) (?v_85 (p2 c_1 c_1 c_0))) (let ((?v_86 (not ?v_85)) (?v_110 (p2 c_1 c_2 c_0))) (let ((?v_88 (not ?v_110)) (?v_140 (p2 c_1 c_3 c_0))) (let ((?v_90 (not ?v_140)) (?v_170 (p2 c_1 c_4 c_0))) (let ((?v_92 (not ?v_170)) (?v_81 (p2 c_1 c_0 c_1))) (let ((?v_77 (not ?v_81)) (?v_94 (p2 c_1 c_1 c_1))) (let ((?v_87 (not ?v_94)) (?v_116 (p2 c_1 c_2 c_1))) (let ((?v_95 (not ?v_116)) (?v_146 (p2 c_1 c_3 c_1))) (let ((?v_96 (not ?v_146)) (?v_176 (p2 c_1 c_4 c_1))) (let ((?v_97 (not ?v_176)) (?v_82 (p2 c_1 c_0 c_2))) (let ((?v_78 (not ?v_82)) (?v_98 (p2 c_1 c_1 c_2))) (let ((?v_89 (not ?v_98)) (?v_122 (p2 c_1 c_2 c_2))) (let ((?v_99 (not ?v_122)) (?v_152 (p2 c_1 c_3 c_2))) (let ((?v_100 (not ?v_152)) (?v_182 (p2 c_1 c_4 c_2))) (let ((?v_101 (not ?v_182)) (?v_83 (p2 c_1 c_0 c_3))) (let ((?v_79 (not ?v_83)) (?v_102 (p2 c_1 c_1 c_3))) (let ((?v_91 (not ?v_102)) (?v_128 (p2 c_1 c_2 c_3))) (let ((?v_103 (not ?v_128)) (?v_158 (p2 c_1 c_3 c_3))) (let ((?v_104 (not ?v_158)) (?v_188 (p2 c_1 c_4 c_3))) (let ((?v_105 (not ?v_188)) (?v_84 (p2 c_1 c_0 c_4))) (let ((?v_80 (not ?v_84)) (?v_106 (p2 c_1 c_1 c_4))) (let ((?v_93 (not ?v_106)) (?v_134 (p2 c_1 c_2 c_4))) (let ((?v_107 (not ?v_134)) (?v_164 (p2 c_1 c_3 c_4))) (let ((?v_108 (not ?v_164)) (?v_194 (p2 c_1 c_4 c_4))) (let ((?v_109 (not ?v_194)) (?v_200 (p2 c_2 c_0 c_0))) (let ((?v_111 (not ?v_200)) (?v_205 (p2 c_2 c_1 c_0))) (let ((?v_112 (not ?v_205)) (?v_210 (p2 c_2 c_2 c_0))) (let ((?v_113 (not ?v_210)) (?v_215 (p2 c_2 c_3 c_0))) (let ((?v_114 (not ?v_215)) (?v_220 (p2 c_2 c_4 c_0))) (let ((?v_115 (not ?v_220)) (?v_201 (p2 c_2 c_0 c_1))) (let ((?v_117 (not ?v_201)) (?v_206 (p2 c_2 c_1 c_1))) (let ((?v_118 (not ?v_206)) (?v_211 (p2 c_2 c_2 c_1))) (let ((?v_119 (not ?v_211)) (?v_216 (p2 c_2 c_3 c_1))) (let ((?v_120 (not ?v_216)) (?v_221 (p2 c_2 c_4 c_1))) (let ((?v_121 (not ?v_221)) (?v_202 (p2 c_2 c_0 c_2))) (let ((?v_123 (not ?v_202)) (?v_207 (p2 c_2 c_1 c_2))) (let ((?v_124 (not ?v_207)) (?v_212 (p2 c_2 c_2 c_2))) (let ((?v_125 (not ?v_212)) (?v_217 (p2 c_2 c_3 c_2))) (let ((?v_126 (not ?v_217)) (?v_222 (p2 c_2 c_4 c_2))) (let ((?v_127 (not ?v_222)) (?v_203 (p2 c_2 c_0 c_3))) (let ((?v_129 (not ?v_203)) (?v_208 (p2 c_2 c_1 c_3))) (let ((?v_130 (not ?v_208)) (?v_213 (p2 c_2 c_2 c_3))) (let ((?v_131 (not ?v_213)) (?v_218 (p2 c_2 c_3 c_3))) (let ((?v_132 (not ?v_218)) (?v_223 (p2 c_2 c_4 c_3))) (let ((?v_133 (not ?v_223)) (?v_204 (p2 c_2 c_0 c_4))) (let ((?v_135 (not ?v_204)) (?v_209 (p2 c_2 c_1 c_4))) (let ((?v_136 (not ?v_209)) (?v_214 (p2 c_2 c_2 c_4))) (let ((?v_137 (not ?v_214)) (?v_219 (p2 c_2 c_3 c_4))) (let ((?v_138 (not ?v_219)) (?v_224 (p2 c_2 c_4 c_4))) (let ((?v_139 (not ?v_224)) (?v_225 (p2 c_3 c_0 c_0))) (let ((?v_141 (not ?v_225)) (?v_230 (p2 c_3 c_1 c_0))) (let ((?v_142 (not ?v_230)) (?v_235 (p2 c_3 c_2 c_0))) (let ((?v_143 (not ?v_235)) (?v_240 (p2 c_3 c_3 c_0))) (let ((?v_144 (not ?v_240)) (?v_245 (p2 c_3 c_4 c_0))) (let ((?v_145 (not ?v_245)) (?v_226 (p2 c_3 c_0 c_1))) (let ((?v_147 (not ?v_226)) (?v_231 (p2 c_3 c_1 c_1))) (let ((?v_148 (not ?v_231)) (?v_236 (p2 c_3 c_2 c_1))) (let ((?v_149 (not ?v_236)) (?v_241 (p2 c_3 c_3 c_1))) (let ((?v_150 (not ?v_241)) (?v_246 (p2 c_3 c_4 c_1))) (let ((?v_151 (not ?v_246)) (?v_227 (p2 c_3 c_0 c_2))) (let ((?v_153 (not ?v_227)) (?v_232 (p2 c_3 c_1 c_2))) (let ((?v_154 (not ?v_232)) (?v_237 (p2 c_3 c_2 c_2))) (let ((?v_155 (not ?v_237)) (?v_242 (p2 c_3 c_3 c_2))) (let ((?v_156 (not ?v_242)) (?v_247 (p2 c_3 c_4 c_2))) (let ((?v_157 (not ?v_247)) (?v_228 (p2 c_3 c_0 c_3))) (let ((?v_159 (not ?v_228)) (?v_233 (p2 c_3 c_1 c_3))) (let ((?v_160 (not ?v_233)) (?v_238 (p2 c_3 c_2 c_3))) (let ((?v_161 (not ?v_238)) (?v_243 (p2 c_3 c_3 c_3))) (let ((?v_162 (not ?v_243)) (?v_248 (p2 c_3 c_4 c_3))) (let ((?v_163 (not ?v_248)) (?v_229 (p2 c_3 c_0 c_4))) (let ((?v_165 (not ?v_229)) (?v_234 (p2 c_3 c_1 c_4))) (let ((?v_166 (not ?v_234)) (?v_239 (p2 c_3 c_2 c_4))) (let ((?v_167 (not ?v_239)) (?v_244 (p2 c_3 c_3 c_4))) (let ((?v_168 (not ?v_244)) (?v_249 (p2 c_3 c_4 c_4))) (let ((?v_169 (not ?v_249)) (?v_250 (p2 c_4 c_0 c_0))) (let ((?v_171 (not ?v_250)) (?v_255 (p2 c_4 c_1 c_0))) (let ((?v_172 (not ?v_255)) (?v_260 (p2 c_4 c_2 c_0))) (let ((?v_173 (not ?v_260)) (?v_265 (p2 c_4 c_3 c_0))) (let ((?v_174 (not ?v_265)) (?v_270 (p2 c_4 c_4 c_0))) (let ((?v_175 (not ?v_270)) (?v_251 (p2 c_4 c_0 c_1))) (let ((?v_177 (not ?v_251)) (?v_256 (p2 c_4 c_1 c_1))) (let ((?v_178 (not ?v_256)) (?v_261 (p2 c_4 c_2 c_1))) (let ((?v_179 (not ?v_261)) (?v_266 (p2 c_4 c_3 c_1))) (let ((?v_180 (not ?v_266)) (?v_271 (p2 c_4 c_4 c_1))) (let ((?v_181 (not ?v_271)) (?v_252 (p2 c_4 c_0 c_2))) (let ((?v_183 (not ?v_252)) (?v_257 (p2 c_4 c_1 c_2))) (let ((?v_184 (not ?v_257)) (?v_262 (p2 c_4 c_2 c_2))) (let ((?v_185 (not ?v_262)) (?v_267 (p2 c_4 c_3 c_2))) (let ((?v_186 (not ?v_267)) (?v_272 (p2 c_4 c_4 c_2))) (let ((?v_187 (not ?v_272)) (?v_253 (p2 c_4 c_0 c_3))) (let ((?v_189 (not ?v_253)) (?v_258 (p2 c_4 c_1 c_3))) (let ((?v_190 (not ?v_258)) (?v_263 (p2 c_4 c_2 c_3))) (let ((?v_191 (not ?v_263)) (?v_268 (p2 c_4 c_3 c_3))) (let ((?v_192 (not ?v_268)) (?v_273 (p2 c_4 c_4 c_3))) (let ((?v_193 (not ?v_273)) (?v_254 (p2 c_4 c_0 c_4))) (let ((?v_195 (not ?v_254)) (?v_259 (p2 c_4 c_1 c_4))) (let ((?v_196 (not ?v_259)) (?v_264 (p2 c_4 c_2 c_4))) (let ((?v_197 (not ?v_264)) (?v_269 (p2 c_4 c_3 c_4))) (let ((?v_198 (not ?v_269)) (?v_274 (p2 c_4 c_4 c_4))) (let ((?v_199 (not ?v_274))) (and (distinct c_0 c_1 c_2 c_3 c_4) ?v_300 (not (= c_0 ?v_280)) (not (= c_0 ?v_285)) (not (= c_0 ?v_290)) (not (= c_0 ?v_295)) (not (= c_1 ?v_276)) ?v_301 (not (= c_1 ?v_286)) (not (= c_1 ?v_291)) (not (= c_1 ?v_296)) (not (= c_2 ?v_277)) (not (= c_2 ?v_282)) ?v_302 (not (= c_2 ?v_292)) (not (= c_2 ?v_297)) (not (= c_3 ?v_278)) (not (= c_3 ?v_283)) (not (= c_3 ?v_288)) ?v_303 (not (= c_3 ?v_298)) (not (= c_4 ?v_279)) (not (= c_4 ?v_284)) (not (= c_4 ?v_289)) (not (= c_4 ?v_294)) ?v_304 (or ?v_0 ?v_1 ?v_2 ?v_1 ?v_1 ?v_2) (or ?v_0 ?v_16 ?v_17 ?v_3 ?v_3 ?v_8) (or ?v_0 ?v_20 ?v_46 ?v_4 ?v_4 ?v_9) (or ?v_0 ?v_23 ?v_56 ?v_5 ?v_5 ?v_10) (or ?v_0 ?v_26 ?v_66 ?v_6 ?v_6 ?v_11) (or ?v_7 ?v_3 ?v_8 ?v_1 ?v_1 ?v_2) (or ?v_7 ?v_18 ?v_19 ?v_3 ?v_3 ?v_8) (or ?v_7 ?v_30 ?v_47 ?v_4 ?v_4 ?v_9) (or ?v_7 ?v_31 ?v_57 ?v_5 ?v_5 ?v_10) (or ?v_7 ?v_32 ?v_67 ?v_6 ?v_6 ?v_11) (or ?v_12 ?v_4 ?v_9 ?v_1 ?v_1 ?v_2) (or ?v_12 ?v_21 ?v_22 ?v_3 ?v_3 ?v_8) (or ?v_12 ?v_34 ?v_48 ?v_4 ?v_4 ?v_9) (or ?v_12 ?v_35 ?v_58 ?v_5 ?v_5 ?v_10) (or ?v_12 ?v_36 ?v_68 ?v_6 ?v_6 ?v_11) (or ?v_13 ?v_5 ?v_10 ?v_1 ?v_1 ?v_2) (or ?v_13 ?v_24 ?v_25 ?v_3 ?v_3 ?v_8) (or ?v_13 ?v_38 ?v_49 ?v_4 ?v_4 ?v_9) (or ?v_13 ?v_39 ?v_59 ?v_5 ?v_5 ?v_10) (or ?v_13 ?v_40 ?v_69 ?v_6 ?v_6 ?v_11) (or ?v_14 ?v_6 ?v_11 ?v_1 ?v_1 ?v_2) (or ?v_14 ?v_27 ?v_28 ?v_3 ?v_3 ?v_8) (or ?v_14 ?v_42 ?v_50 ?v_4 ?v_4 ?v_9) (or ?v_14 ?v_43 ?v_60 ?v_5 ?v_5 ?v_10) (or ?v_14 ?v_44 ?v_70 ?v_6 ?v_6 ?v_11) (or ?v_15 ?v_1 ?v_76 ?v_16 ?v_1 ?v_17) (or ?v_15 ?v_16 ?v_86 ?v_18 ?v_3 ?v_19) (or ?v_15 ?v_20 ?v_88 ?v_21 ?v_4 ?v_22) (or ?v_15 ?v_23 ?v_90 ?v_24 ?v_5 ?v_25) (or ?v_15 ?v_26 ?v_92 ?v_27 ?v_6 ?v_28) (or ?v_29 ?v_3 ?v_77 ?v_16 ?v_1 ?v_17) (or ?v_29 ?v_18 ?v_87 ?v_18 ?v_3 ?v_19) (or ?v_29 ?v_30 ?v_95 ?v_21 ?v_4 ?v_22) (or ?v_29 ?v_31 ?v_96 ?v_24 ?v_5 ?v_25) (or ?v_29 ?v_32 ?v_97 ?v_27 ?v_6 ?v_28) (or ?v_33 ?v_4 ?v_78 ?v_16 ?v_1 ?v_17) (or ?v_33 ?v_21 ?v_89 ?v_18 ?v_3 ?v_19) (or ?v_33 ?v_34 ?v_99 ?v_21 ?v_4 ?v_22) (or ?v_33 ?v_35 ?v_100 ?v_24 ?v_5 ?v_25) (or ?v_33 ?v_36 ?v_101 ?v_27 ?v_6 ?v_28) (or ?v_37 ?v_5 ?v_79 ?v_16 ?v_1 ?v_17) (or ?v_37 ?v_24 ?v_91 ?v_18 ?v_3 ?v_19) (or ?v_37 ?v_38 ?v_103 ?v_21 ?v_4 ?v_22) (or ?v_37 ?v_39 ?v_104 ?v_24 ?v_5 ?v_25) (or ?v_37 ?v_40 ?v_105 ?v_27 ?v_6 ?v_28) (or ?v_41 ?v_6 ?v_80 ?v_16 ?v_1 ?v_17) (or ?v_41 ?v_27 ?v_93 ?v_18 ?v_3 ?v_19) (or ?v_41 ?v_42 ?v_107 ?v_21 ?v_4 ?v_22) (or ?v_41 ?v_43 ?v_108 ?v_24 ?v_5 ?v_25) (or ?v_41 ?v_44 ?v_109 ?v_27 ?v_6 ?v_28) (or ?v_45 ?v_1 ?v_111 ?v_20 ?v_1 ?v_46) (or ?v_45 ?v_16 ?v_112 ?v_30 ?v_3 ?v_47) (or ?v_45 ?v_20 ?v_113 ?v_34 ?v_4 ?v_48) (or ?v_45 ?v_23 ?v_114 ?v_38 ?v_5 ?v_49) (or ?v_45 ?v_26 ?v_115 ?v_42 ?v_6 ?v_50) (or ?v_51 ?v_3 ?v_117 ?v_20 ?v_1 ?v_46) (or ?v_51 ?v_18 ?v_118 ?v_30 ?v_3 ?v_47) (or ?v_51 ?v_30 ?v_119 ?v_34 ?v_4 ?v_48) (or ?v_51 ?v_31 ?v_120 ?v_38 ?v_5 ?v_49) (or ?v_51 ?v_32 ?v_121 ?v_42 ?v_6 ?v_50) (or ?v_52 ?v_4 ?v_123 ?v_20 ?v_1 ?v_46) (or ?v_52 ?v_21 ?v_124 ?v_30 ?v_3 ?v_47) (or ?v_52 ?v_34 ?v_125 ?v_34 ?v_4 ?v_48) (or ?v_52 ?v_35 ?v_126 ?v_38 ?v_5 ?v_49) (or ?v_52 ?v_36 ?v_127 ?v_42 ?v_6 ?v_50) (or ?v_53 ?v_5 ?v_129 ?v_20 ?v_1 ?v_46) (or ?v_53 ?v_24 ?v_130 ?v_30 ?v_3 ?v_47) (or ?v_53 ?v_38 ?v_131 ?v_34 ?v_4 ?v_48) (or ?v_53 ?v_39 ?v_132 ?v_38 ?v_5 ?v_49) (or ?v_53 ?v_40 ?v_133 ?v_42 ?v_6 ?v_50) (or ?v_54 ?v_6 ?v_135 ?v_20 ?v_1 ?v_46) (or ?v_54 ?v_27 ?v_136 ?v_30 ?v_3 ?v_47) (or ?v_54 ?v_42 ?v_137 ?v_34 ?v_4 ?v_48) (or ?v_54 ?v_43 ?v_138 ?v_38 ?v_5 ?v_49) (or ?v_54 ?v_44 ?v_139 ?v_42 ?v_6 ?v_50) (or ?v_55 ?v_1 ?v_141 ?v_23 ?v_1 ?v_56) (or ?v_55 ?v_16 ?v_142 ?v_31 ?v_3 ?v_57) (or ?v_55 ?v_20 ?v_143 ?v_35 ?v_4 ?v_58) (or ?v_55 ?v_23 ?v_144 ?v_39 ?v_5 ?v_59) (or ?v_55 ?v_26 ?v_145 ?v_43 ?v_6 ?v_60) (or ?v_61 ?v_3 ?v_147 ?v_23 ?v_1 ?v_56) (or ?v_61 ?v_18 ?v_148 ?v_31 ?v_3 ?v_57) (or ?v_61 ?v_30 ?v_149 ?v_35 ?v_4 ?v_58) (or ?v_61 ?v_31 ?v_150 ?v_39 ?v_5 ?v_59) (or ?v_61 ?v_32 ?v_151 ?v_43 ?v_6 ?v_60) (or ?v_62 ?v_4 ?v_153 ?v_23 ?v_1 ?v_56) (or ?v_62 ?v_21 ?v_154 ?v_31 ?v_3 ?v_57) (or ?v_62 ?v_34 ?v_155 ?v_35 ?v_4 ?v_58) (or ?v_62 ?v_35 ?v_156 ?v_39 ?v_5 ?v_59) (or ?v_62 ?v_36 ?v_157 ?v_43 ?v_6 ?v_60) (or ?v_63 ?v_5 ?v_159 ?v_23 ?v_1 ?v_56) (or ?v_63 ?v_24 ?v_160 ?v_31 ?v_3 ?v_57) (or ?v_63 ?v_38 ?v_161 ?v_35 ?v_4 ?v_58) (or ?v_63 ?v_39 ?v_162 ?v_39 ?v_5 ?v_59) (or ?v_63 ?v_40 ?v_163 ?v_43 ?v_6 ?v_60) (or ?v_64 ?v_6 ?v_165 ?v_23 ?v_1 ?v_56) (or ?v_64 ?v_27 ?v_166 ?v_31 ?v_3 ?v_57) (or ?v_64 ?v_42 ?v_167 ?v_35 ?v_4 ?v_58) (or ?v_64 ?v_43 ?v_168 ?v_39 ?v_5 ?v_59) (or ?v_64 ?v_44 ?v_169 ?v_43 ?v_6 ?v_60) (or ?v_65 ?v_1 ?v_171 ?v_26 ?v_1 ?v_66) (or ?v_65 ?v_16 ?v_172 ?v_32 ?v_3 ?v_67) (or ?v_65 ?v_20 ?v_173 ?v_36 ?v_4 ?v_68) (or ?v_65 ?v_23 ?v_174 ?v_40 ?v_5 ?v_69) (or ?v_65 ?v_26 ?v_175 ?v_44 ?v_6 ?v_70) (or ?v_71 ?v_3 ?v_177 ?v_26 ?v_1 ?v_66) (or ?v_71 ?v_18 ?v_178 ?v_32 ?v_3 ?v_67) (or ?v_71 ?v_30 ?v_179 ?v_36 ?v_4 ?v_68) (or ?v_71 ?v_31 ?v_180 ?v_40 ?v_5 ?v_69) (or ?v_71 ?v_32 ?v_181 ?v_44 ?v_6 ?v_70) (or ?v_72 ?v_4 ?v_183 ?v_26 ?v_1 ?v_66) (or ?v_72 ?v_21 ?v_184 ?v_32 ?v_3 ?v_67) (or ?v_72 ?v_34 ?v_185 ?v_36 ?v_4 ?v_68) (or ?v_72 ?v_35 ?v_186 ?v_40 ?v_5 ?v_69) (or ?v_72 ?v_36 ?v_187 ?v_44 ?v_6 ?v_70) (or ?v_73 ?v_5 ?v_189 ?v_26 ?v_1 ?v_66) (or ?v_73 ?v_24 ?v_190 ?v_32 ?v_3 ?v_67) (or ?v_73 ?v_38 ?v_191 ?v_36 ?v_4 ?v_68) (or ?v_73 ?v_39 ?v_192 ?v_40 ?v_5 ?v_69) (or ?v_73 ?v_40 ?v_193 ?v_44 ?v_6 ?v_70) (or ?v_74 ?v_6 ?v_195 ?v_26 ?v_1 ?v_66) (or ?v_74 ?v_27 ?v_196 ?v_32 ?v_3 ?v_67) (or ?v_74 ?v_42 ?v_197 ?v_36 ?v_4 ?v_68) (or ?v_74 ?v_43 ?v_198 ?v_40 ?v_5 ?v_69) (or ?v_74 ?v_44 ?v_199 ?v_44 ?v_6 ?v_70) (or ?v_75 ?v_1 ?v_2 ?v_1 ?v_16 ?v_76) (or ?v_75 ?v_16 ?v_17 ?v_3 ?v_18 ?v_77) (or ?v_75 ?v_20 ?v_46 ?v_4 ?v_21 ?v_78) (or ?v_75 ?v_23 ?v_56 ?v_5 ?v_24 ?v_79) (or ?v_75 ?v_26 ?v_66 ?v_6 ?v_27 ?v_80) (or ?v_81 ?v_3 ?v_8 ?v_1 ?v_16 ?v_76) (or ?v_81 ?v_18 ?v_19 ?v_3 ?v_18 ?v_77) (or ?v_81 ?v_30 ?v_47 ?v_4 ?v_21 ?v_78) (or ?v_81 ?v_31 ?v_57 ?v_5 ?v_24 ?v_79) (or ?v_81 ?v_32 ?v_67 ?v_6 ?v_27 ?v_80) (or ?v_82 ?v_4 ?v_9 ?v_1 ?v_16 ?v_76) (or ?v_82 ?v_21 ?v_22 ?v_3 ?v_18 ?v_77) (or ?v_82 ?v_34 ?v_48 ?v_4 ?v_21 ?v_78) (or ?v_82 ?v_35 ?v_58 ?v_5 ?v_24 ?v_79) (or ?v_82 ?v_36 ?v_68 ?v_6 ?v_27 ?v_80) (or ?v_83 ?v_5 ?v_10 ?v_1 ?v_16 ?v_76) (or ?v_83 ?v_24 ?v_25 ?v_3 ?v_18 ?v_77) (or ?v_83 ?v_38 ?v_49 ?v_4 ?v_21 ?v_78) (or ?v_83 ?v_39 ?v_59 ?v_5 ?v_24 ?v_79) (or ?v_83 ?v_40 ?v_69 ?v_6 ?v_27 ?v_80) (or ?v_84 ?v_6 ?v_11 ?v_1 ?v_16 ?v_76) (or ?v_84 ?v_27 ?v_28 ?v_3 ?v_18 ?v_77) (or ?v_84 ?v_42 ?v_50 ?v_4 ?v_21 ?v_78) (or ?v_84 ?v_43 ?v_60 ?v_5 ?v_24 ?v_79) (or ?v_84 ?v_44 ?v_70 ?v_6 ?v_27 ?v_80) (or ?v_85 ?v_1 ?v_76 ?v_16 ?v_16 ?v_86) (or ?v_85 ?v_16 ?v_86 ?v_18 ?v_18 ?v_87) (or ?v_85 ?v_20 ?v_88 ?v_21 ?v_21 ?v_89) (or ?v_85 ?v_23 ?v_90 ?v_24 ?v_24 ?v_91) (or ?v_85 ?v_26 ?v_92 ?v_27 ?v_27 ?v_93) (or ?v_94 ?v_3 ?v_77 ?v_16 ?v_16 ?v_86) (or ?v_94 ?v_18 ?v_87 ?v_18 ?v_18 ?v_87) (or ?v_94 ?v_30 ?v_95 ?v_21 ?v_21 ?v_89) (or ?v_94 ?v_31 ?v_96 ?v_24 ?v_24 ?v_91) (or ?v_94 ?v_32 ?v_97 ?v_27 ?v_27 ?v_93) (or ?v_98 ?v_4 ?v_78 ?v_16 ?v_16 ?v_86) (or ?v_98 ?v_21 ?v_89 ?v_18 ?v_18 ?v_87) (or ?v_98 ?v_34 ?v_99 ?v_21 ?v_21 ?v_89) (or ?v_98 ?v_35 ?v_100 ?v_24 ?v_24 ?v_91) (or ?v_98 ?v_36 ?v_101 ?v_27 ?v_27 ?v_93) (or ?v_102 ?v_5 ?v_79 ?v_16 ?v_16 ?v_86) (or ?v_102 ?v_24 ?v_91 ?v_18 ?v_18 ?v_87) (or ?v_102 ?v_38 ?v_103 ?v_21 ?v_21 ?v_89) (or ?v_102 ?v_39 ?v_104 ?v_24 ?v_24 ?v_91) (or ?v_102 ?v_40 ?v_105 ?v_27 ?v_27 ?v_93) (or ?v_106 ?v_6 ?v_80 ?v_16 ?v_16 ?v_86) (or ?v_106 ?v_27 ?v_93 ?v_18 ?v_18 ?v_87) (or ?v_106 ?v_42 ?v_107 ?v_21 ?v_21 ?v_89) (or ?v_106 ?v_43 ?v_108 ?v_24 ?v_24 ?v_91) (or ?v_106 ?v_44 ?v_109 ?v_27 ?v_27 ?v_93) (or ?v_110 ?v_1 ?v_111 ?v_20 ?v_16 ?v_88) (or ?v_110 ?v_16 ?v_112 ?v_30 ?v_18 ?v_95) (or ?v_110 ?v_20 ?v_113 ?v_34 ?v_21 ?v_99) (or ?v_110 ?v_23 ?v_114 ?v_38 ?v_24 ?v_103) (or ?v_110 ?v_26 ?v_115 ?v_42 ?v_27 ?v_107) (or ?v_116 ?v_3 ?v_117 ?v_20 ?v_16 ?v_88) (or ?v_116 ?v_18 ?v_118 ?v_30 ?v_18 ?v_95) (or ?v_116 ?v_30 ?v_119 ?v_34 ?v_21 ?v_99) (or ?v_116 ?v_31 ?v_120 ?v_38 ?v_24 ?v_103) (or ?v_116 ?v_32 ?v_121 ?v_42 ?v_27 ?v_107) (or ?v_122 ?v_4 ?v_123 ?v_20 ?v_16 ?v_88) (or ?v_122 ?v_21 ?v_124 ?v_30 ?v_18 ?v_95) (or ?v_122 ?v_34 ?v_125 ?v_34 ?v_21 ?v_99) (or ?v_122 ?v_35 ?v_126 ?v_38 ?v_24 ?v_103) (or ?v_122 ?v_36 ?v_127 ?v_42 ?v_27 ?v_107) (or ?v_128 ?v_5 ?v_129 ?v_20 ?v_16 ?v_88) (or ?v_128 ?v_24 ?v_130 ?v_30 ?v_18 ?v_95) (or ?v_128 ?v_38 ?v_131 ?v_34 ?v_21 ?v_99) (or ?v_128 ?v_39 ?v_132 ?v_38 ?v_24 ?v_103) (or ?v_128 ?v_40 ?v_133 ?v_42 ?v_27 ?v_107) (or ?v_134 ?v_6 ?v_135 ?v_20 ?v_16 ?v_88) (or ?v_134 ?v_27 ?v_136 ?v_30 ?v_18 ?v_95) (or ?v_134 ?v_42 ?v_137 ?v_34 ?v_21 ?v_99) (or ?v_134 ?v_43 ?v_138 ?v_38 ?v_24 ?v_103) (or ?v_134 ?v_44 ?v_139 ?v_42 ?v_27 ?v_107) (or ?v_140 ?v_1 ?v_141 ?v_23 ?v_16 ?v_90) (or ?v_140 ?v_16 ?v_142 ?v_31 ?v_18 ?v_96) (or ?v_140 ?v_20 ?v_143 ?v_35 ?v_21 ?v_100) (or ?v_140 ?v_23 ?v_144 ?v_39 ?v_24 ?v_104) (or ?v_140 ?v_26 ?v_145 ?v_43 ?v_27 ?v_108) (or ?v_146 ?v_3 ?v_147 ?v_23 ?v_16 ?v_90) (or ?v_146 ?v_18 ?v_148 ?v_31 ?v_18 ?v_96) (or ?v_146 ?v_30 ?v_149 ?v_35 ?v_21 ?v_100) (or ?v_146 ?v_31 ?v_150 ?v_39 ?v_24 ?v_104) (or ?v_146 ?v_32 ?v_151 ?v_43 ?v_27 ?v_108) (or ?v_152 ?v_4 ?v_153 ?v_23 ?v_16 ?v_90) (or ?v_152 ?v_21 ?v_154 ?v_31 ?v_18 ?v_96) (or ?v_152 ?v_34 ?v_155 ?v_35 ?v_21 ?v_100) (or ?v_152 ?v_35 ?v_156 ?v_39 ?v_24 ?v_104) (or ?v_152 ?v_36 ?v_157 ?v_43 ?v_27 ?v_108) (or ?v_158 ?v_5 ?v_159 ?v_23 ?v_16 ?v_90) (or ?v_158 ?v_24 ?v_160 ?v_31 ?v_18 ?v_96) (or ?v_158 ?v_38 ?v_161 ?v_35 ?v_21 ?v_100) (or ?v_158 ?v_39 ?v_162 ?v_39 ?v_24 ?v_104) (or ?v_158 ?v_40 ?v_163 ?v_43 ?v_27 ?v_108) (or ?v_164 ?v_6 ?v_165 ?v_23 ?v_16 ?v_90) (or ?v_164 ?v_27 ?v_166 ?v_31 ?v_18 ?v_96) (or ?v_164 ?v_42 ?v_167 ?v_35 ?v_21 ?v_100) (or ?v_164 ?v_43 ?v_168 ?v_39 ?v_24 ?v_104) (or ?v_164 ?v_44 ?v_169 ?v_43 ?v_27 ?v_108) (or ?v_170 ?v_1 ?v_171 ?v_26 ?v_16 ?v_92) (or ?v_170 ?v_16 ?v_172 ?v_32 ?v_18 ?v_97) (or ?v_170 ?v_20 ?v_173 ?v_36 ?v_21 ?v_101) (or ?v_170 ?v_23 ?v_174 ?v_40 ?v_24 ?v_105) (or ?v_170 ?v_26 ?v_175 ?v_44 ?v_27 ?v_109) (or ?v_176 ?v_3 ?v_177 ?v_26 ?v_16 ?v_92) (or ?v_176 ?v_18 ?v_178 ?v_32 ?v_18 ?v_97) (or ?v_176 ?v_30 ?v_179 ?v_36 ?v_21 ?v_101) (or ?v_176 ?v_31 ?v_180 ?v_40 ?v_24 ?v_105) (or ?v_176 ?v_32 ?v_181 ?v_44 ?v_27 ?v_109) (or ?v_182 ?v_4 ?v_183 ?v_26 ?v_16 ?v_92) (or ?v_182 ?v_21 ?v_184 ?v_32 ?v_18 ?v_97) (or ?v_182 ?v_34 ?v_185 ?v_36 ?v_21 ?v_101) (or ?v_182 ?v_35 ?v_186 ?v_40 ?v_24 ?v_105) (or ?v_182 ?v_36 ?v_187 ?v_44 ?v_27 ?v_109) (or ?v_188 ?v_5 ?v_189 ?v_26 ?v_16 ?v_92) (or ?v_188 ?v_24 ?v_190 ?v_32 ?v_18 ?v_97) (or ?v_188 ?v_38 ?v_191 ?v_36 ?v_21 ?v_101) (or ?v_188 ?v_39 ?v_192 ?v_40 ?v_24 ?v_105) (or ?v_188 ?v_40 ?v_193 ?v_44 ?v_27 ?v_109) (or ?v_194 ?v_6 ?v_195 ?v_26 ?v_16 ?v_92) (or ?v_194 ?v_27 ?v_196 ?v_32 ?v_18 ?v_97) (or ?v_194 ?v_42 ?v_197 ?v_36 ?v_21 ?v_101) (or ?v_194 ?v_43 ?v_198 ?v_40 ?v_24 ?v_105) (or ?v_194 ?v_44 ?v_199 ?v_44 ?v_27 ?v_109) (or ?v_200 ?v_1 ?v_2 ?v_1 ?v_20 ?v_111) (or ?v_200 ?v_16 ?v_17 ?v_3 ?v_30 ?v_117) (or ?v_200 ?v_20 ?v_46 ?v_4 ?v_34 ?v_123) (or ?v_200 ?v_23 ?v_56 ?v_5 ?v_38 ?v_129) (or ?v_200 ?v_26 ?v_66 ?v_6 ?v_42 ?v_135) (or ?v_201 ?v_3 ?v_8 ?v_1 ?v_20 ?v_111) (or ?v_201 ?v_18 ?v_19 ?v_3 ?v_30 ?v_117) (or ?v_201 ?v_30 ?v_47 ?v_4 ?v_34 ?v_123) (or ?v_201 ?v_31 ?v_57 ?v_5 ?v_38 ?v_129) (or ?v_201 ?v_32 ?v_67 ?v_6 ?v_42 ?v_135) (or ?v_202 ?v_4 ?v_9 ?v_1 ?v_20 ?v_111) (or ?v_202 ?v_21 ?v_22 ?v_3 ?v_30 ?v_117) (or ?v_202 ?v_34 ?v_48 ?v_4 ?v_34 ?v_123) (or ?v_202 ?v_35 ?v_58 ?v_5 ?v_38 ?v_129) (or ?v_202 ?v_36 ?v_68 ?v_6 ?v_42 ?v_135) (or ?v_203 ?v_5 ?v_10 ?v_1 ?v_20 ?v_111) (or ?v_203 ?v_24 ?v_25 ?v_3 ?v_30 ?v_117) (or ?v_203 ?v_38 ?v_49 ?v_4 ?v_34 ?v_123) (or ?v_203 ?v_39 ?v_59 ?v_5 ?v_38 ?v_129) (or ?v_203 ?v_40 ?v_69 ?v_6 ?v_42 ?v_135) (or ?v_204 ?v_6 ?v_11 ?v_1 ?v_20 ?v_111) (or ?v_204 ?v_27 ?v_28 ?v_3 ?v_30 ?v_117) (or ?v_204 ?v_42 ?v_50 ?v_4 ?v_34 ?v_123) (or ?v_204 ?v_43 ?v_60 ?v_5 ?v_38 ?v_129) (or ?v_204 ?v_44 ?v_70 ?v_6 ?v_42 ?v_135) (or ?v_205 ?v_1 ?v_76 ?v_16 ?v_20 ?v_112) (or ?v_205 ?v_16 ?v_86 ?v_18 ?v_30 ?v_118) (or ?v_205 ?v_20 ?v_88 ?v_21 ?v_34 ?v_124) (or ?v_205 ?v_23 ?v_90 ?v_24 ?v_38 ?v_130) (or ?v_205 ?v_26 ?v_92 ?v_27 ?v_42 ?v_136) (or ?v_206 ?v_3 ?v_77 ?v_16 ?v_20 ?v_112) (or ?v_206 ?v_18 ?v_87 ?v_18 ?v_30 ?v_118) (or ?v_206 ?v_30 ?v_95 ?v_21 ?v_34 ?v_124) (or ?v_206 ?v_31 ?v_96 ?v_24 ?v_38 ?v_130) (or ?v_206 ?v_32 ?v_97 ?v_27 ?v_42 ?v_136) (or ?v_207 ?v_4 ?v_78 ?v_16 ?v_20 ?v_112) (or ?v_207 ?v_21 ?v_89 ?v_18 ?v_30 ?v_118) (or ?v_207 ?v_34 ?v_99 ?v_21 ?v_34 ?v_124) (or ?v_207 ?v_35 ?v_100 ?v_24 ?v_38 ?v_130) (or ?v_207 ?v_36 ?v_101 ?v_27 ?v_42 ?v_136) (or ?v_208 ?v_5 ?v_79 ?v_16 ?v_20 ?v_112) (or ?v_208 ?v_24 ?v_91 ?v_18 ?v_30 ?v_118) (or ?v_208 ?v_38 ?v_103 ?v_21 ?v_34 ?v_124) (or ?v_208 ?v_39 ?v_104 ?v_24 ?v_38 ?v_130) (or ?v_208 ?v_40 ?v_105 ?v_27 ?v_42 ?v_136) (or ?v_209 ?v_6 ?v_80 ?v_16 ?v_20 ?v_112) (or ?v_209 ?v_27 ?v_93 ?v_18 ?v_30 ?v_118) (or ?v_209 ?v_42 ?v_107 ?v_21 ?v_34 ?v_124) (or ?v_209 ?v_43 ?v_108 ?v_24 ?v_38 ?v_130) (or ?v_209 ?v_44 ?v_109 ?v_27 ?v_42 ?v_136) (or ?v_210 ?v_1 ?v_111 ?v_20 ?v_20 ?v_113) (or ?v_210 ?v_16 ?v_112 ?v_30 ?v_30 ?v_119) (or ?v_210 ?v_20 ?v_113 ?v_34 ?v_34 ?v_125) (or ?v_210 ?v_23 ?v_114 ?v_38 ?v_38 ?v_131) (or ?v_210 ?v_26 ?v_115 ?v_42 ?v_42 ?v_137) (or ?v_211 ?v_3 ?v_117 ?v_20 ?v_20 ?v_113) (or ?v_211 ?v_18 ?v_118 ?v_30 ?v_30 ?v_119) (or ?v_211 ?v_30 ?v_119 ?v_34 ?v_34 ?v_125) (or ?v_211 ?v_31 ?v_120 ?v_38 ?v_38 ?v_131) (or ?v_211 ?v_32 ?v_121 ?v_42 ?v_42 ?v_137) (or ?v_212 ?v_4 ?v_123 ?v_20 ?v_20 ?v_113) (or ?v_212 ?v_21 ?v_124 ?v_30 ?v_30 ?v_119) (or ?v_212 ?v_34 ?v_125 ?v_34 ?v_34 ?v_125) (or ?v_212 ?v_35 ?v_126 ?v_38 ?v_38 ?v_131) (or ?v_212 ?v_36 ?v_127 ?v_42 ?v_42 ?v_137) (or ?v_213 ?v_5 ?v_129 ?v_20 ?v_20 ?v_113) (or ?v_213 ?v_24 ?v_130 ?v_30 ?v_30 ?v_119) (or ?v_213 ?v_38 ?v_131 ?v_34 ?v_34 ?v_125) (or ?v_213 ?v_39 ?v_132 ?v_38 ?v_38 ?v_131) (or ?v_213 ?v_40 ?v_133 ?v_42 ?v_42 ?v_137) (or ?v_214 ?v_6 ?v_135 ?v_20 ?v_20 ?v_113) (or ?v_214 ?v_27 ?v_136 ?v_30 ?v_30 ?v_119) (or ?v_214 ?v_42 ?v_137 ?v_34 ?v_34 ?v_125) (or ?v_214 ?v_43 ?v_138 ?v_38 ?v_38 ?v_131) (or ?v_214 ?v_44 ?v_139 ?v_42 ?v_42 ?v_137) (or ?v_215 ?v_1 ?v_141 ?v_23 ?v_20 ?v_114) (or ?v_215 ?v_16 ?v_142 ?v_31 ?v_30 ?v_120) (or ?v_215 ?v_20 ?v_143 ?v_35 ?v_34 ?v_126) (or ?v_215 ?v_23 ?v_144 ?v_39 ?v_38 ?v_132) (or ?v_215 ?v_26 ?v_145 ?v_43 ?v_42 ?v_138) (or ?v_216 ?v_3 ?v_147 ?v_23 ?v_20 ?v_114) (or ?v_216 ?v_18 ?v_148 ?v_31 ?v_30 ?v_120) (or ?v_216 ?v_30 ?v_149 ?v_35 ?v_34 ?v_126) (or ?v_216 ?v_31 ?v_150 ?v_39 ?v_38 ?v_132) (or ?v_216 ?v_32 ?v_151 ?v_43 ?v_42 ?v_138) (or ?v_217 ?v_4 ?v_153 ?v_23 ?v_20 ?v_114) (or ?v_217 ?v_21 ?v_154 ?v_31 ?v_30 ?v_120) (or ?v_217 ?v_34 ?v_155 ?v_35 ?v_34 ?v_126) (or ?v_217 ?v_35 ?v_156 ?v_39 ?v_38 ?v_132) (or ?v_217 ?v_36 ?v_157 ?v_43 ?v_42 ?v_138) (or ?v_218 ?v_5 ?v_159 ?v_23 ?v_20 ?v_114) (or ?v_218 ?v_24 ?v_160 ?v_31 ?v_30 ?v_120) (or ?v_218 ?v_38 ?v_161 ?v_35 ?v_34 ?v_126) (or ?v_218 ?v_39 ?v_162 ?v_39 ?v_38 ?v_132) (or ?v_218 ?v_40 ?v_163 ?v_43 ?v_42 ?v_138) (or ?v_219 ?v_6 ?v_165 ?v_23 ?v_20 ?v_114) (or ?v_219 ?v_27 ?v_166 ?v_31 ?v_30 ?v_120) (or ?v_219 ?v_42 ?v_167 ?v_35 ?v_34 ?v_126) (or ?v_219 ?v_43 ?v_168 ?v_39 ?v_38 ?v_132) (or ?v_219 ?v_44 ?v_169 ?v_43 ?v_42 ?v_138) (or ?v_220 ?v_1 ?v_171 ?v_26 ?v_20 ?v_115) (or ?v_220 ?v_16 ?v_172 ?v_32 ?v_30 ?v_121) (or ?v_220 ?v_20 ?v_173 ?v_36 ?v_34 ?v_127) (or ?v_220 ?v_23 ?v_174 ?v_40 ?v_38 ?v_133) (or ?v_220 ?v_26 ?v_175 ?v_44 ?v_42 ?v_139) (or ?v_221 ?v_3 ?v_177 ?v_26 ?v_20 ?v_115) (or ?v_221 ?v_18 ?v_178 ?v_32 ?v_30 ?v_121) (or ?v_221 ?v_30 ?v_179 ?v_36 ?v_34 ?v_127) (or ?v_221 ?v_31 ?v_180 ?v_40 ?v_38 ?v_133) (or ?v_221 ?v_32 ?v_181 ?v_44 ?v_42 ?v_139) (or ?v_222 ?v_4 ?v_183 ?v_26 ?v_20 ?v_115) (or ?v_222 ?v_21 ?v_184 ?v_32 ?v_30 ?v_121) (or ?v_222 ?v_34 ?v_185 ?v_36 ?v_34 ?v_127) (or ?v_222 ?v_35 ?v_186 ?v_40 ?v_38 ?v_133) (or ?v_222 ?v_36 ?v_187 ?v_44 ?v_42 ?v_139) (or ?v_223 ?v_5 ?v_189 ?v_26 ?v_20 ?v_115) (or ?v_223 ?v_24 ?v_190 ?v_32 ?v_30 ?v_121) (or ?v_223 ?v_38 ?v_191 ?v_36 ?v_34 ?v_127) (or ?v_223 ?v_39 ?v_192 ?v_40 ?v_38 ?v_133) (or ?v_223 ?v_40 ?v_193 ?v_44 ?v_42 ?v_139) (or ?v_224 ?v_6 ?v_195 ?v_26 ?v_20 ?v_115) (or ?v_224 ?v_27 ?v_196 ?v_32 ?v_30 ?v_121) (or ?v_224 ?v_42 ?v_197 ?v_36 ?v_34 ?v_127) (or ?v_224 ?v_43 ?v_198 ?v_40 ?v_38 ?v_133) (or ?v_224 ?v_44 ?v_199 ?v_44 ?v_42 ?v_139) (or ?v_225 ?v_1 ?v_2 ?v_1 ?v_23 ?v_141) (or ?v_225 ?v_16 ?v_17 ?v_3 ?v_31 ?v_147) (or ?v_225 ?v_20 ?v_46 ?v_4 ?v_35 ?v_153) (or ?v_225 ?v_23 ?v_56 ?v_5 ?v_39 ?v_159) (or ?v_225 ?v_26 ?v_66 ?v_6 ?v_43 ?v_165) (or ?v_226 ?v_3 ?v_8 ?v_1 ?v_23 ?v_141) (or ?v_226 ?v_18 ?v_19 ?v_3 ?v_31 ?v_147) (or ?v_226 ?v_30 ?v_47 ?v_4 ?v_35 ?v_153) (or ?v_226 ?v_31 ?v_57 ?v_5 ?v_39 ?v_159) (or ?v_226 ?v_32 ?v_67 ?v_6 ?v_43 ?v_165) (or ?v_227 ?v_4 ?v_9 ?v_1 ?v_23 ?v_141) (or ?v_227 ?v_21 ?v_22 ?v_3 ?v_31 ?v_147) (or ?v_227 ?v_34 ?v_48 ?v_4 ?v_35 ?v_153) (or ?v_227 ?v_35 ?v_58 ?v_5 ?v_39 ?v_159) (or ?v_227 ?v_36 ?v_68 ?v_6 ?v_43 ?v_165) (or ?v_228 ?v_5 ?v_10 ?v_1 ?v_23 ?v_141) (or ?v_228 ?v_24 ?v_25 ?v_3 ?v_31 ?v_147) (or ?v_228 ?v_38 ?v_49 ?v_4 ?v_35 ?v_153) (or ?v_228 ?v_39 ?v_59 ?v_5 ?v_39 ?v_159) (or ?v_228 ?v_40 ?v_69 ?v_6 ?v_43 ?v_165) (or ?v_229 ?v_6 ?v_11 ?v_1 ?v_23 ?v_141) (or ?v_229 ?v_27 ?v_28 ?v_3 ?v_31 ?v_147) (or ?v_229 ?v_42 ?v_50 ?v_4 ?v_35 ?v_153) (or ?v_229 ?v_43 ?v_60 ?v_5 ?v_39 ?v_159) (or ?v_229 ?v_44 ?v_70 ?v_6 ?v_43 ?v_165) (or ?v_230 ?v_1 ?v_76 ?v_16 ?v_23 ?v_142) (or ?v_230 ?v_16 ?v_86 ?v_18 ?v_31 ?v_148) (or ?v_230 ?v_20 ?v_88 ?v_21 ?v_35 ?v_154) (or ?v_230 ?v_23 ?v_90 ?v_24 ?v_39 ?v_160) (or ?v_230 ?v_26 ?v_92 ?v_27 ?v_43 ?v_166) (or ?v_231 ?v_3 ?v_77 ?v_16 ?v_23 ?v_142) (or ?v_231 ?v_18 ?v_87 ?v_18 ?v_31 ?v_148) (or ?v_231 ?v_30 ?v_95 ?v_21 ?v_35 ?v_154) (or ?v_231 ?v_31 ?v_96 ?v_24 ?v_39 ?v_160) (or ?v_231 ?v_32 ?v_97 ?v_27 ?v_43 ?v_166) (or ?v_232 ?v_4 ?v_78 ?v_16 ?v_23 ?v_142) (or ?v_232 ?v_21 ?v_89 ?v_18 ?v_31 ?v_148) (or ?v_232 ?v_34 ?v_99 ?v_21 ?v_35 ?v_154) (or ?v_232 ?v_35 ?v_100 ?v_24 ?v_39 ?v_160) (or ?v_232 ?v_36 ?v_101 ?v_27 ?v_43 ?v_166) (or ?v_233 ?v_5 ?v_79 ?v_16 ?v_23 ?v_142) (or ?v_233 ?v_24 ?v_91 ?v_18 ?v_31 ?v_148) (or ?v_233 ?v_38 ?v_103 ?v_21 ?v_35 ?v_154) (or ?v_233 ?v_39 ?v_104 ?v_24 ?v_39 ?v_160) (or ?v_233 ?v_40 ?v_105 ?v_27 ?v_43 ?v_166) (or ?v_234 ?v_6 ?v_80 ?v_16 ?v_23 ?v_142) (or ?v_234 ?v_27 ?v_93 ?v_18 ?v_31 ?v_148) (or ?v_234 ?v_42 ?v_107 ?v_21 ?v_35 ?v_154) (or ?v_234 ?v_43 ?v_108 ?v_24 ?v_39 ?v_160) (or ?v_234 ?v_44 ?v_109 ?v_27 ?v_43 ?v_166) (or ?v_235 ?v_1 ?v_111 ?v_20 ?v_23 ?v_143) (or ?v_235 ?v_16 ?v_112 ?v_30 ?v_31 ?v_149) (or ?v_235 ?v_20 ?v_113 ?v_34 ?v_35 ?v_155) (or ?v_235 ?v_23 ?v_114 ?v_38 ?v_39 ?v_161) (or ?v_235 ?v_26 ?v_115 ?v_42 ?v_43 ?v_167) (or ?v_236 ?v_3 ?v_117 ?v_20 ?v_23 ?v_143) (or ?v_236 ?v_18 ?v_118 ?v_30 ?v_31 ?v_149) (or ?v_236 ?v_30 ?v_119 ?v_34 ?v_35 ?v_155) (or ?v_236 ?v_31 ?v_120 ?v_38 ?v_39 ?v_161) (or ?v_236 ?v_32 ?v_121 ?v_42 ?v_43 ?v_167) (or ?v_237 ?v_4 ?v_123 ?v_20 ?v_23 ?v_143) (or ?v_237 ?v_21 ?v_124 ?v_30 ?v_31 ?v_149) (or ?v_237 ?v_34 ?v_125 ?v_34 ?v_35 ?v_155) (or ?v_237 ?v_35 ?v_126 ?v_38 ?v_39 ?v_161) (or ?v_237 ?v_36 ?v_127 ?v_42 ?v_43 ?v_167) (or ?v_238 ?v_5 ?v_129 ?v_20 ?v_23 ?v_143) (or ?v_238 ?v_24 ?v_130 ?v_30 ?v_31 ?v_149) (or ?v_238 ?v_38 ?v_131 ?v_34 ?v_35 ?v_155) (or ?v_238 ?v_39 ?v_132 ?v_38 ?v_39 ?v_161) (or ?v_238 ?v_40 ?v_133 ?v_42 ?v_43 ?v_167) (or ?v_239 ?v_6 ?v_135 ?v_20 ?v_23 ?v_143) (or ?v_239 ?v_27 ?v_136 ?v_30 ?v_31 ?v_149) (or ?v_239 ?v_42 ?v_137 ?v_34 ?v_35 ?v_155) (or ?v_239 ?v_43 ?v_138 ?v_38 ?v_39 ?v_161) (or ?v_239 ?v_44 ?v_139 ?v_42 ?v_43 ?v_167) (or ?v_240 ?v_1 ?v_141 ?v_23 ?v_23 ?v_144) (or ?v_240 ?v_16 ?v_142 ?v_31 ?v_31 ?v_150) (or ?v_240 ?v_20 ?v_143 ?v_35 ?v_35 ?v_156) (or ?v_240 ?v_23 ?v_144 ?v_39 ?v_39 ?v_162) (or ?v_240 ?v_26 ?v_145 ?v_43 ?v_43 ?v_168) (or ?v_241 ?v_3 ?v_147 ?v_23 ?v_23 ?v_144) (or ?v_241 ?v_18 ?v_148 ?v_31 ?v_31 ?v_150) (or ?v_241 ?v_30 ?v_149 ?v_35 ?v_35 ?v_156) (or ?v_241 ?v_31 ?v_150 ?v_39 ?v_39 ?v_162) (or ?v_241 ?v_32 ?v_151 ?v_43 ?v_43 ?v_168) (or ?v_242 ?v_4 ?v_153 ?v_23 ?v_23 ?v_144) (or ?v_242 ?v_21 ?v_154 ?v_31 ?v_31 ?v_150) (or ?v_242 ?v_34 ?v_155 ?v_35 ?v_35 ?v_156) (or ?v_242 ?v_35 ?v_156 ?v_39 ?v_39 ?v_162) (or ?v_242 ?v_36 ?v_157 ?v_43 ?v_43 ?v_168) (or ?v_243 ?v_5 ?v_159 ?v_23 ?v_23 ?v_144) (or ?v_243 ?v_24 ?v_160 ?v_31 ?v_31 ?v_150) (or ?v_243 ?v_38 ?v_161 ?v_35 ?v_35 ?v_156) (or ?v_243 ?v_39 ?v_162 ?v_39 ?v_39 ?v_162) (or ?v_243 ?v_40 ?v_163 ?v_43 ?v_43 ?v_168) (or ?v_244 ?v_6 ?v_165 ?v_23 ?v_23 ?v_144) (or ?v_244 ?v_27 ?v_166 ?v_31 ?v_31 ?v_150) (or ?v_244 ?v_42 ?v_167 ?v_35 ?v_35 ?v_156) (or ?v_244 ?v_43 ?v_168 ?v_39 ?v_39 ?v_162) (or ?v_244 ?v_44 ?v_169 ?v_43 ?v_43 ?v_168) (or ?v_245 ?v_1 ?v_171 ?v_26 ?v_23 ?v_145) (or ?v_245 ?v_16 ?v_172 ?v_32 ?v_31 ?v_151) (or ?v_245 ?v_20 ?v_173 ?v_36 ?v_35 ?v_157) (or ?v_245 ?v_23 ?v_174 ?v_40 ?v_39 ?v_163) (or ?v_245 ?v_26 ?v_175 ?v_44 ?v_43 ?v_169) (or ?v_246 ?v_3 ?v_177 ?v_26 ?v_23 ?v_145) (or ?v_246 ?v_18 ?v_178 ?v_32 ?v_31 ?v_151) (or ?v_246 ?v_30 ?v_179 ?v_36 ?v_35 ?v_157) (or ?v_246 ?v_31 ?v_180 ?v_40 ?v_39 ?v_163) (or ?v_246 ?v_32 ?v_181 ?v_44 ?v_43 ?v_169) (or ?v_247 ?v_4 ?v_183 ?v_26 ?v_23 ?v_145) (or ?v_247 ?v_21 ?v_184 ?v_32 ?v_31 ?v_151) (or ?v_247 ?v_34 ?v_185 ?v_36 ?v_35 ?v_157) (or ?v_247 ?v_35 ?v_186 ?v_40 ?v_39 ?v_163) (or ?v_247 ?v_36 ?v_187 ?v_44 ?v_43 ?v_169) (or ?v_248 ?v_5 ?v_189 ?v_26 ?v_23 ?v_145) (or ?v_248 ?v_24 ?v_190 ?v_32 ?v_31 ?v_151) (or ?v_248 ?v_38 ?v_191 ?v_36 ?v_35 ?v_157) (or ?v_248 ?v_39 ?v_192 ?v_40 ?v_39 ?v_163) (or ?v_248 ?v_40 ?v_193 ?v_44 ?v_43 ?v_169) (or ?v_249 ?v_6 ?v_195 ?v_26 ?v_23 ?v_145) (or ?v_249 ?v_27 ?v_196 ?v_32 ?v_31 ?v_151) (or ?v_249 ?v_42 ?v_197 ?v_36 ?v_35 ?v_157) (or ?v_249 ?v_43 ?v_198 ?v_40 ?v_39 ?v_163) (or ?v_249 ?v_44 ?v_199 ?v_44 ?v_43 ?v_169) (or ?v_250 ?v_1 ?v_2 ?v_1 ?v_26 ?v_171) (or ?v_250 ?v_16 ?v_17 ?v_3 ?v_32 ?v_177) (or ?v_250 ?v_20 ?v_46 ?v_4 ?v_36 ?v_183) (or ?v_250 ?v_23 ?v_56 ?v_5 ?v_40 ?v_189) (or ?v_250 ?v_26 ?v_66 ?v_6 ?v_44 ?v_195) (or ?v_251 ?v_3 ?v_8 ?v_1 ?v_26 ?v_171) (or ?v_251 ?v_18 ?v_19 ?v_3 ?v_32 ?v_177) (or ?v_251 ?v_30 ?v_47 ?v_4 ?v_36 ?v_183) (or ?v_251 ?v_31 ?v_57 ?v_5 ?v_40 ?v_189) (or ?v_251 ?v_32 ?v_67 ?v_6 ?v_44 ?v_195) (or ?v_252 ?v_4 ?v_9 ?v_1 ?v_26 ?v_171) (or ?v_252 ?v_21 ?v_22 ?v_3 ?v_32 ?v_177) (or ?v_252 ?v_34 ?v_48 ?v_4 ?v_36 ?v_183) (or ?v_252 ?v_35 ?v_58 ?v_5 ?v_40 ?v_189) (or ?v_252 ?v_36 ?v_68 ?v_6 ?v_44 ?v_195) (or ?v_253 ?v_5 ?v_10 ?v_1 ?v_26 ?v_171) (or ?v_253 ?v_24 ?v_25 ?v_3 ?v_32 ?v_177) (or ?v_253 ?v_38 ?v_49 ?v_4 ?v_36 ?v_183) (or ?v_253 ?v_39 ?v_59 ?v_5 ?v_40 ?v_189) (or ?v_253 ?v_40 ?v_69 ?v_6 ?v_44 ?v_195) (or ?v_254 ?v_6 ?v_11 ?v_1 ?v_26 ?v_171) (or ?v_254 ?v_27 ?v_28 ?v_3 ?v_32 ?v_177) (or ?v_254 ?v_42 ?v_50 ?v_4 ?v_36 ?v_183) (or ?v_254 ?v_43 ?v_60 ?v_5 ?v_40 ?v_189) (or ?v_254 ?v_44 ?v_70 ?v_6 ?v_44 ?v_195) (or ?v_255 ?v_1 ?v_76 ?v_16 ?v_26 ?v_172) (or ?v_255 ?v_16 ?v_86 ?v_18 ?v_32 ?v_178) (or ?v_255 ?v_20 ?v_88 ?v_21 ?v_36 ?v_184) (or ?v_255 ?v_23 ?v_90 ?v_24 ?v_40 ?v_190) (or ?v_255 ?v_26 ?v_92 ?v_27 ?v_44 ?v_196) (or ?v_256 ?v_3 ?v_77 ?v_16 ?v_26 ?v_172) (or ?v_256 ?v_18 ?v_87 ?v_18 ?v_32 ?v_178) (or ?v_256 ?v_30 ?v_95 ?v_21 ?v_36 ?v_184) (or ?v_256 ?v_31 ?v_96 ?v_24 ?v_40 ?v_190) (or ?v_256 ?v_32 ?v_97 ?v_27 ?v_44 ?v_196) (or ?v_257 ?v_4 ?v_78 ?v_16 ?v_26 ?v_172) (or ?v_257 ?v_21 ?v_89 ?v_18 ?v_32 ?v_178) (or ?v_257 ?v_34 ?v_99 ?v_21 ?v_36 ?v_184) (or ?v_257 ?v_35 ?v_100 ?v_24 ?v_40 ?v_190) (or ?v_257 ?v_36 ?v_101 ?v_27 ?v_44 ?v_196) (or ?v_258 ?v_5 ?v_79 ?v_16 ?v_26 ?v_172) (or ?v_258 ?v_24 ?v_91 ?v_18 ?v_32 ?v_178) (or ?v_258 ?v_38 ?v_103 ?v_21 ?v_36 ?v_184) (or ?v_258 ?v_39 ?v_104 ?v_24 ?v_40 ?v_190) (or ?v_258 ?v_40 ?v_105 ?v_27 ?v_44 ?v_196) (or ?v_259 ?v_6 ?v_80 ?v_16 ?v_26 ?v_172) (or ?v_259 ?v_27 ?v_93 ?v_18 ?v_32 ?v_178) (or ?v_259 ?v_42 ?v_107 ?v_21 ?v_36 ?v_184) (or ?v_259 ?v_43 ?v_108 ?v_24 ?v_40 ?v_190) (or ?v_259 ?v_44 ?v_109 ?v_27 ?v_44 ?v_196) (or ?v_260 ?v_1 ?v_111 ?v_20 ?v_26 ?v_173) (or ?v_260 ?v_16 ?v_112 ?v_30 ?v_32 ?v_179) (or ?v_260 ?v_20 ?v_113 ?v_34 ?v_36 ?v_185) (or ?v_260 ?v_23 ?v_114 ?v_38 ?v_40 ?v_191) (or ?v_260 ?v_26 ?v_115 ?v_42 ?v_44 ?v_197) (or ?v_261 ?v_3 ?v_117 ?v_20 ?v_26 ?v_173) (or ?v_261 ?v_18 ?v_118 ?v_30 ?v_32 ?v_179) (or ?v_261 ?v_30 ?v_119 ?v_34 ?v_36 ?v_185) (or ?v_261 ?v_31 ?v_120 ?v_38 ?v_40 ?v_191) (or ?v_261 ?v_32 ?v_121 ?v_42 ?v_44 ?v_197) (or ?v_262 ?v_4 ?v_123 ?v_20 ?v_26 ?v_173) (or ?v_262 ?v_21 ?v_124 ?v_30 ?v_32 ?v_179) (or ?v_262 ?v_34 ?v_125 ?v_34 ?v_36 ?v_185) (or ?v_262 ?v_35 ?v_126 ?v_38 ?v_40 ?v_191) (or ?v_262 ?v_36 ?v_127 ?v_42 ?v_44 ?v_197) (or ?v_263 ?v_5 ?v_129 ?v_20 ?v_26 ?v_173) (or ?v_263 ?v_24 ?v_130 ?v_30 ?v_32 ?v_179) (or ?v_263 ?v_38 ?v_131 ?v_34 ?v_36 ?v_185) (or ?v_263 ?v_39 ?v_132 ?v_38 ?v_40 ?v_191) (or ?v_263 ?v_40 ?v_133 ?v_42 ?v_44 ?v_197) (or ?v_264 ?v_6 ?v_135 ?v_20 ?v_26 ?v_173) (or ?v_264 ?v_27 ?v_136 ?v_30 ?v_32 ?v_179) (or ?v_264 ?v_42 ?v_137 ?v_34 ?v_36 ?v_185) (or ?v_264 ?v_43 ?v_138 ?v_38 ?v_40 ?v_191) (or ?v_264 ?v_44 ?v_139 ?v_42 ?v_44 ?v_197) (or ?v_265 ?v_1 ?v_141 ?v_23 ?v_26 ?v_174) (or ?v_265 ?v_16 ?v_142 ?v_31 ?v_32 ?v_180) (or ?v_265 ?v_20 ?v_143 ?v_35 ?v_36 ?v_186) (or ?v_265 ?v_23 ?v_144 ?v_39 ?v_40 ?v_192) (or ?v_265 ?v_26 ?v_145 ?v_43 ?v_44 ?v_198) (or ?v_266 ?v_3 ?v_147 ?v_23 ?v_26 ?v_174) (or ?v_266 ?v_18 ?v_148 ?v_31 ?v_32 ?v_180) (or ?v_266 ?v_30 ?v_149 ?v_35 ?v_36 ?v_186) (or ?v_266 ?v_31 ?v_150 ?v_39 ?v_40 ?v_192) (or ?v_266 ?v_32 ?v_151 ?v_43 ?v_44 ?v_198) (or ?v_267 ?v_4 ?v_153 ?v_23 ?v_26 ?v_174) (or ?v_267 ?v_21 ?v_154 ?v_31 ?v_32 ?v_180) (or ?v_267 ?v_34 ?v_155 ?v_35 ?v_36 ?v_186) (or ?v_267 ?v_35 ?v_156 ?v_39 ?v_40 ?v_192) (or ?v_267 ?v_36 ?v_157 ?v_43 ?v_44 ?v_198) (or ?v_268 ?v_5 ?v_159 ?v_23 ?v_26 ?v_174) (or ?v_268 ?v_24 ?v_160 ?v_31 ?v_32 ?v_180) (or ?v_268 ?v_38 ?v_161 ?v_35 ?v_36 ?v_186) (or ?v_268 ?v_39 ?v_162 ?v_39 ?v_40 ?v_192) (or ?v_268 ?v_40 ?v_163 ?v_43 ?v_44 ?v_198) (or ?v_269 ?v_6 ?v_165 ?v_23 ?v_26 ?v_174) (or ?v_269 ?v_27 ?v_166 ?v_31 ?v_32 ?v_180) (or ?v_269 ?v_42 ?v_167 ?v_35 ?v_36 ?v_186) (or ?v_269 ?v_43 ?v_168 ?v_39 ?v_40 ?v_192) (or ?v_269 ?v_44 ?v_169 ?v_43 ?v_44 ?v_198) (or ?v_270 ?v_1 ?v_171 ?v_26 ?v_26 ?v_175) (or ?v_270 ?v_16 ?v_172 ?v_32 ?v_32 ?v_181) (or ?v_270 ?v_20 ?v_173 ?v_36 ?v_36 ?v_187) (or ?v_270 ?v_23 ?v_174 ?v_40 ?v_40 ?v_193) (or ?v_270 ?v_26 ?v_175 ?v_44 ?v_44 ?v_199) (or ?v_271 ?v_3 ?v_177 ?v_26 ?v_26 ?v_175) (or ?v_271 ?v_18 ?v_178 ?v_32 ?v_32 ?v_181) (or ?v_271 ?v_30 ?v_179 ?v_36 ?v_36 ?v_187) (or ?v_271 ?v_31 ?v_180 ?v_40 ?v_40 ?v_193) (or ?v_271 ?v_32 ?v_181 ?v_44 ?v_44 ?v_199) (or ?v_272 ?v_4 ?v_183 ?v_26 ?v_26 ?v_175) (or ?v_272 ?v_21 ?v_184 ?v_32 ?v_32 ?v_181) (or ?v_272 ?v_34 ?v_185 ?v_36 ?v_36 ?v_187) (or ?v_272 ?v_35 ?v_186 ?v_40 ?v_40 ?v_193) (or ?v_272 ?v_36 ?v_187 ?v_44 ?v_44 ?v_199) (or ?v_273 ?v_5 ?v_189 ?v_26 ?v_26 ?v_175) (or ?v_273 ?v_24 ?v_190 ?v_32 ?v_32 ?v_181) (or ?v_273 ?v_38 ?v_191 ?v_36 ?v_36 ?v_187) (or ?v_273 ?v_39 ?v_192 ?v_40 ?v_40 ?v_193) (or ?v_273 ?v_40 ?v_193 ?v_44 ?v_44 ?v_199) (or ?v_274 ?v_6 ?v_195 ?v_26 ?v_26 ?v_175) (or ?v_274 ?v_27 ?v_196 ?v_32 ?v_32 ?v_181) (or ?v_274 ?v_42 ?v_197 ?v_36 ?v_36 ?v_187) (or ?v_274 ?v_43 ?v_198 ?v_40 ?v_40 ?v_193) (or ?v_274 ?v_44 ?v_199 ?v_44 ?v_44 ?v_199) (p2 c_0 c_0 ?v_275) (p2 c_0 c_1 ?v_276) (p2 c_0 c_2 ?v_277) (p2 c_0 c_3 ?v_278) (p2 c_0 c_4 ?v_279) (p2 c_1 c_0 ?v_280) (p2 c_1 c_1 ?v_281) (p2 c_1 c_2 ?v_282) (p2 c_1 c_3 ?v_283) (p2 c_1 c_4 ?v_284) (p2 c_2 c_0 ?v_285) (p2 c_2 c_1 ?v_286) (p2 c_2 c_2 ?v_287) (p2 c_2 c_3 ?v_288) (p2 c_2 c_4 ?v_289) (p2 c_3 c_0 ?v_290) (p2 c_3 c_1 ?v_291) (p2 c_3 c_2 ?v_292) (p2 c_3 c_3 ?v_293) (p2 c_3 c_4 ?v_294) (p2 c_4 c_0 ?v_295) (p2 c_4 c_1 ?v_296) (p2 c_4 c_2 ?v_297) (p2 c_4 c_3 ?v_298) (p2 c_4 c_4 ?v_299) (or ?v_0 ?v_2) (or ?v_7 ?v_8) (or ?v_12 ?v_9) (or ?v_13 ?v_10) (or ?v_14 ?v_11) (or ?v_15 ?v_76) (or ?v_29 ?v_77) (or ?v_33 ?v_78) (or ?v_37 ?v_79) (or ?v_41 ?v_80) (or ?v_45 ?v_111) (or ?v_51 ?v_117) (or ?v_52 ?v_123) (or ?v_53 ?v_129) (or ?v_54 ?v_135) (or ?v_55 ?v_141) (or ?v_61 ?v_147) (or ?v_62 ?v_153) (or ?v_63 ?v_159) (or ?v_64 ?v_165) (or ?v_65 ?v_171) (or ?v_71 ?v_177) (or ?v_72 ?v_183) (or ?v_73 ?v_189) (or ?v_74 ?v_195) (or ?v_75 ?v_17) (or ?v_81 ?v_19) (or ?v_82 ?v_22) (or ?v_83 ?v_25) (or ?v_84 ?v_28) (or ?v_85 ?v_86) (or ?v_94 ?v_87) (or ?v_98 ?v_89) (or ?v_102 ?v_91) (or ?v_106 ?v_93) (or ?v_110 ?v_112) (or ?v_116 ?v_118) (or ?v_122 ?v_124) (or ?v_128 ?v_130) (or ?v_134 ?v_136) (or ?v_140 ?v_142) (or ?v_146 ?v_148) (or ?v_152 ?v_154) (or ?v_158 ?v_160) (or ?v_164 ?v_166) (or ?v_170 ?v_172) (or ?v_176 ?v_178) (or ?v_182 ?v_184) (or ?v_188 ?v_190) (or ?v_194 ?v_196) (or ?v_200 ?v_46) (or ?v_201 ?v_47) (or ?v_202 ?v_48) (or ?v_203 ?v_49) (or ?v_204 ?v_50) (or ?v_205 ?v_88) (or ?v_206 ?v_95) (or ?v_207 ?v_99) (or ?v_208 ?v_103) (or ?v_209 ?v_107) (or ?v_210 ?v_113) (or ?v_211 ?v_119) (or ?v_212 ?v_125) (or ?v_213 ?v_131) (or ?v_214 ?v_137) (or ?v_215 ?v_143) (or ?v_216 ?v_149) (or ?v_217 ?v_155) (or ?v_218 ?v_161) (or ?v_219 ?v_167) (or ?v_220 ?v_173) (or ?v_221 ?v_179) (or ?v_222 ?v_185) (or ?v_223 ?v_191) (or ?v_224 ?v_197) (or ?v_225 ?v_56) (or ?v_226 ?v_57) (or ?v_227 ?v_58) (or ?v_228 ?v_59) (or ?v_229 ?v_60) (or ?v_230 ?v_90) (or ?v_231 ?v_96) (or ?v_232 ?v_100) (or ?v_233 ?v_104) (or ?v_234 ?v_108) (or ?v_235 ?v_114) (or ?v_236 ?v_120) (or ?v_237 ?v_126) (or ?v_238 ?v_132) (or ?v_239 ?v_138) (or ?v_240 ?v_144) (or ?v_241 ?v_150) (or ?v_242 ?v_156) (or ?v_243 ?v_162) (or ?v_244 ?v_168) (or ?v_245 ?v_174) (or ?v_246 ?v_180) (or ?v_247 ?v_186) (or ?v_248 ?v_192) (or ?v_249 ?v_198) (or ?v_250 ?v_66) (or ?v_251 ?v_67) (or ?v_252 ?v_68) (or ?v_253 ?v_69) (or ?v_254 ?v_70) (or ?v_255 ?v_92) (or ?v_256 ?v_97) (or ?v_257 ?v_101) (or ?v_258 ?v_105) (or ?v_259 ?v_109) (or ?v_260 ?v_115) (or ?v_261 ?v_121) (or ?v_262 ?v_127) (or ?v_263 ?v_133) (or ?v_264 ?v_139) (or ?v_265 ?v_145) (or ?v_266 ?v_151) (or ?v_267 ?v_157) (or ?v_268 ?v_163) (or ?v_269 ?v_169) (or ?v_270 ?v_175) (or ?v_271 ?v_181) (or ?v_272 ?v_187) (or ?v_273 ?v_193) (or ?v_274 ?v_199) ?v_0 ?v_7 ?v_12 ?v_13 ?v_14 ?v_85 ?v_94 ?v_98 ?v_102 ?v_106 ?v_210 ?v_211 ?v_212 ?v_213 ?v_214 ?v_240 ?v_241 ?v_242 ?v_243 ?v_244 ?v_270 ?v_271 ?v_272 ?v_273 ?v_274 (not (p2 c3 c4 c5)) (or ?v_2 ?v_0) (or ?v_8 ?v_75) (or ?v_9 ?v_200) (or ?v_10 ?v_225) (or ?v_11 ?v_250) (or ?v_17 ?v_7) (or ?v_19 ?v_81) (or ?v_22 ?v_201) (or ?v_25 ?v_226) (or ?v_28 ?v_251) (or ?v_46 ?v_12) (or ?v_47 ?v_82) (or ?v_48 ?v_202) (or ?v_49 ?v_227) (or ?v_50 ?v_252) (or ?v_56 ?v_13) (or ?v_57 ?v_83) (or ?v_58 ?v_203) (or ?v_59 ?v_228) (or ?v_60 ?v_253) (or ?v_66 ?v_14) (or ?v_67 ?v_84) (or ?v_68 ?v_204) (or ?v_69 ?v_229) (or ?v_70 ?v_254) (or ?v_76 ?v_15) (or ?v_77 ?v_85) (or ?v_78 ?v_205) (or ?v_79 ?v_230) (or ?v_80 ?v_255) (or ?v_86 ?v_29) (or ?v_87 ?v_94) (or ?v_89 ?v_206) (or ?v_91 ?v_231) (or ?v_93 ?v_256) (or ?v_88 ?v_33) (or ?v_95 ?v_98) (or ?v_99 ?v_207) (or ?v_103 ?v_232) (or ?v_107 ?v_257) (or ?v_90 ?v_37) (or ?v_96 ?v_102) (or ?v_100 ?v_208) (or ?v_104 ?v_233) (or ?v_108 ?v_258) (or ?v_92 ?v_41) (or ?v_97 ?v_106) (or ?v_101 ?v_209) (or ?v_105 ?v_234) (or ?v_109 ?v_259) (or ?v_111 ?v_45) (or ?v_117 ?v_110) (or ?v_123 ?v_210) (or ?v_129 ?v_235) (or ?v_135 ?v_260) (or ?v_112 ?v_51) (or ?v_118 ?v_116) (or ?v_124 ?v_211) (or ?v_130 ?v_236) (or ?v_136 ?v_261) (or ?v_113 ?v_52) (or ?v_119 ?v_122) (or ?v_125 ?v_212) (or ?v_131 ?v_237) (or ?v_137 ?v_262) (or ?v_114 ?v_53) (or ?v_120 ?v_128) (or ?v_126 ?v_213) (or ?v_132 ?v_238) (or ?v_138 ?v_263) (or ?v_115 ?v_54) (or ?v_121 ?v_134) (or ?v_127 ?v_214) (or ?v_133 ?v_239) (or ?v_139 ?v_264) (or ?v_141 ?v_55) (or ?v_147 ?v_140) (or ?v_153 ?v_215) (or ?v_159 ?v_240) (or ?v_165 ?v_265) (or ?v_142 ?v_61) (or ?v_148 ?v_146) (or ?v_154 ?v_216) (or ?v_160 ?v_241) (or ?v_166 ?v_266) (or ?v_143 ?v_62) (or ?v_149 ?v_152) (or ?v_155 ?v_217) (or ?v_161 ?v_242) (or ?v_167 ?v_267) (or ?v_144 ?v_63) (or ?v_150 ?v_158) (or ?v_156 ?v_218) (or ?v_162 ?v_243) (or ?v_168 ?v_268) (or ?v_145 ?v_64) (or ?v_151 ?v_164) (or ?v_157 ?v_219) (or ?v_163 ?v_244) (or ?v_169 ?v_269) (or ?v_171 ?v_65) (or ?v_177 ?v_170) (or ?v_183 ?v_220) (or ?v_189 ?v_245) (or ?v_195 ?v_270) (or ?v_172 ?v_71) (or ?v_178 ?v_176) (or ?v_184 ?v_221) (or ?v_190 ?v_246) (or ?v_196 ?v_271) (or ?v_173 ?v_72) (or ?v_179 ?v_182) (or ?v_185 ?v_222) (or ?v_191 ?v_247) (or ?v_197 ?v_272) (or ?v_174 ?v_73) (or ?v_180 ?v_188) (or ?v_186 ?v_223) (or ?v_192 ?v_248) (or ?v_198 ?v_273) (or ?v_175 ?v_74) (or ?v_181 ?v_194) (or ?v_187 ?v_224) (or ?v_193 ?v_249) (or ?v_199 ?v_274) ?v_300 (not (= c_0 ?v_276)) (not (= c_0 ?v_277)) (not (= c_0 ?v_278)) (not (= c_0 ?v_279)) (not (= c_1 ?v_280)) ?v_301 (not (= c_1 ?v_282)) (not (= c_1 ?v_283)) (not (= c_1 ?v_284)) (not (= c_2 ?v_285)) (not (= c_2 ?v_286)) ?v_302 (not (= c_2 ?v_288)) (not (= c_2 ?v_289)) (not (= c_3 ?v_290)) (not (= c_3 ?v_291)) (not (= c_3 ?v_292)) ?v_303 (not (= c_3 ?v_294)) (not (= c_4 ?v_295)) (not (= c_4 ?v_296)) (not (= c_4 ?v_297)) (not (= c_4 ?v_298)) ?v_304 (or (= ?v_275 c_0) (= ?v_275 c_1) (= ?v_275 c_2) (= ?v_275 c_3) (= ?v_275 c_4)) (or (= ?v_276 c_0) (= ?v_276 c_1) (= ?v_276 c_2) (= ?v_276 c_3) (= ?v_276 c_4)) (or (= ?v_277 c_0) (= ?v_277 c_1) (= ?v_277 c_2) (= ?v_277 c_3) (= ?v_277 c_4)) (or (= ?v_278 c_0) (= ?v_278 c_1) (= ?v_278 c_2) (= ?v_278 c_3) (= ?v_278 c_4)) (or (= ?v_279 c_0) (= ?v_279 c_1) (= ?v_279 c_2) (= ?v_279 c_3) (= ?v_279 c_4)) (or (= ?v_280 c_0) (= ?v_280 c_1) (= ?v_280 c_2) (= ?v_280 c_3) (= ?v_280 c_4)) (or (= ?v_281 c_0) (= ?v_281 c_1) (= ?v_281 c_2) (= ?v_281 c_3) (= ?v_281 c_4)) (or (= ?v_282 c_0) (= ?v_282 c_1) (= ?v_282 c_2) (= ?v_282 c_3) (= ?v_282 c_4)) (or (= ?v_283 c_0) (= ?v_283 c_1) (= ?v_283 c_2) (= ?v_283 c_3) (= ?v_283 c_4)) (or (= ?v_284 c_0) (= ?v_284 c_1) (= ?v_284 c_2) (= ?v_284 c_3) (= ?v_284 c_4)) (or (= ?v_285 c_0) (= ?v_285 c_1) (= ?v_285 c_2) (= ?v_285 c_3) (= ?v_285 c_4)) (or (= ?v_286 c_0) (= ?v_286 c_1) (= ?v_286 c_2) (= ?v_286 c_3) (= ?v_286 c_4)) (or (= ?v_287 c_0) (= ?v_287 c_1) (= ?v_287 c_2) (= ?v_287 c_3) (= ?v_287 c_4)) (or (= ?v_288 c_0) (= ?v_288 c_1) (= ?v_288 c_2) (= ?v_288 c_3) (= ?v_288 c_4)) (or (= ?v_289 c_0) (= ?v_289 c_1) (= ?v_289 c_2) (= ?v_289 c_3) (= ?v_289 c_4)) (or (= ?v_290 c_0) (= ?v_290 c_1) (= ?v_290 c_2) (= ?v_290 c_3) (= ?v_290 c_4)) (or (= ?v_291 c_0) (= ?v_291 c_1) (= ?v_291 c_2) (= ?v_291 c_3) (= ?v_291 c_4)) (or (= ?v_292 c_0) (= ?v_292 c_1) (= ?v_292 c_2) (= ?v_292 c_3) (= ?v_292 c_4)) (or (= ?v_293 c_0) (= ?v_293 c_1) (= ?v_293 c_2) (= ?v_293 c_3) (= ?v_293 c_4)) (or (= ?v_294 c_0) (= ?v_294 c_1) (= ?v_294 c_2) (= ?v_294 c_3) (= ?v_294 c_4)) (or (= ?v_295 c_0) (= ?v_295 c_1) (= ?v_295 c_2) (= ?v_295 c_3) (= ?v_295 c_4)) (or (= ?v_296 c_0) (= ?v_296 c_1) (= ?v_296 c_2) (= ?v_296 c_3) (= ?v_296 c_4)) (or (= ?v_297 c_0) (= ?v_297 c_1) (= ?v_297 c_2) (= ?v_297 c_3) (= ?v_297 c_4)) (or (= ?v_298 c_0) (= ?v_298 c_1) (= ?v_298 c_2) (= ?v_298 c_3) (= ?v_298 c_4)) (or (= ?v_299 c_0) (= ?v_299 c_1) (= ?v_299 c_2) (= ?v_299 c_3) (= ?v_299 c_4)) (or (= c3 c_0) (= c3 c_1) (= c3 c_2) (= c3 c_3) (= c3 c_4)) (or (= c4 c_0) (= c4 c_1) (= c4 c_2) (= c4 c_3) (= c4 c_4)) (or (= c5 c_0) (= c5 c_1) (= c5 c_2) (= c5 c_3) (= c5 c_4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
